T:Type, L:(T List), x:T. (x  L)  ((x = last(L)))  x before last(L)  L 

latex

ProofTree

Definitions	t  T, x:A. B(x), P  Q, x before y  l, x. t(x), P  Q, P  Q, P & Q, P  Q, , True, if b then t else f fi , ff, null(as), b, A, {T}, T, tt, i <z j, b, i z j, nth_tl(n;as), hd(l), Y, ||as||, l[i], last(L), False, x(s)
Lemmas	l member wf, nil member, cons sublist cons, cons member, implies functionality wrt iff, all functionality wrt iff, sublist wf, last wf, not wf, false wf, last cons, true wf, squash wf, null wf, assert wf, assert of null, member iff sublist, last member